%
% symbolic.pro --- symbolic three-layer analysis
%

portray((X,Y)):- write('('), write(X), write(','), write(Y), write(')').

secs([],[]).
secs([(_,Y)|LST],[Y|LSTP]) :- secs(LST,LSTP).

zip([],[],[]).
zip([X1|LST1],[X2|LST2],[(X1,X2)|LST]) :- zip(LST1,LST2,LST).

putfam(_,[],[]).
putfam(FAM,[X|LST],[XP|LSTP]) :- putfam(FAM,X,XP), putfam(FAM,LST,LSTP).
putfam(FAM,pri(T,LST),pri(T,LSTP)) :- putfam(FAM,LST,LSTP).
putfam(FAM,cm(V,A,B),cm((V,FAM),A,B)).
putfam(FAM,cmr(V,A,B),cmr((V,FAM),A,B)).


actsx(dot,[]) :- !.
actsx(bot,[]) :- !.
actsx(LST,LST).
acts(cm(_,ACTA,ACTB),LST) :- actsx(ACTA,LSTA), actsx(ACTB,LSTB), append(LSTA,LSTB,LST).
acts(cmr(_,ACTA,ACTB),LST) :- actsx(ACTA,LSTA), actsx(ACTB,LSTB), append(LSTA,LSTB,LST).

% ----- possible content equivalence ------------------------------------------

% piecewise
pwcecext([],[],[]). pwcecext([X1|LST1],[X2|LST2],CEC) :- cecextt(X1,X2,CEC1), pwcecextt(LST1,LST2,CEC2), append(CEC1,CEC2,CEC).
% cm <-> cm
cecext(X,Y,[mp(X,Y)]) :- X=cmr(V,dot,bot), !, Y=cmr(V,dot,bot).
cecext(X,Y,[mp(X,Y)]) :- Y=cmr(_,dot,bot), !, fail.
cecext(X,Y,[mp(X,Y)]) :- X=cmr(V,_,_), !, Y=cmr(V,_,_).
cecext(X,Y,[mp(X,Y)]) :- Y=cmr(_,_,_), !, fail.
cecext(X,Y,[mp(X,Y)]) :- X=cm(_,_,_), Y=cm(_,_,_), !.
% prim <-> prim
cecext(pri(T1,LST1),pri(T2,LST2),CEC) :- T1\=lst, T1\=(sum,_), T2\=lst, T2\=(sum,_), !, T1=T2, pwcecextt(LST1,LST2,CEC).
% reduce prilist to list
cecext(pri(lst,LST1),pri(lst,LST2),CEC) :- !, cecextt(LST1,LST2,CEC).
cecext(pri(lst,LST1),M2,CEC) :- !, cecextt(LST1,M2,CEC).
cecext(M1,pri(lst,LST2),CEC) :- !, cecextt(M1,LST2,CEC).
% sum <-> sum
cecext(M1,M2,[mp(M1,M2)]) :- M1=pri((sum,_),[_]),  M2=pri((sum,_),[_]), !.
% sum <-> cm/prim
cecext(M1,M2,[mp(M1,M2)|CEC]) :- M1=pri((sum,F),[X1]), not(is_list(M2)), !, putfam(F,X1,X1F), cecextt(X1F,M2,CEC).
cecext(M1,M2,[mp(M1,M2)|CEC]) :- M2=pri((sum,F),[X2]), not(is_list(M1)), !, putfam(F,X2,X2F), cecextt(M1,X2F,CEC).
% other cases
cecext(cm(_,_,_),_,_) :- !, fail.
cecext(_,cm(_,_,_),_) :- !, fail.
cecext(cmr(_,_,_),_,_) :- !, fail.
cecext(_,cmr(_,_,_),_) :- !, fail.
% we have now handled all cases except that the two are not lists
cecext(A,B,_) :- not(is_list(A)), not(is_list(B)), !, print('*** Assertion failed: A, B both not lists: '), print(A), print(' vs '), print(B), print('\n'), fail.
% list and item
cecext(A,LST,CEC) :- A=pri((sum,_),_), !, cecextt([A],LST,CEC).
cecext(LST,B,CEC) :- B=pri((sum,_),_), !, cecextt(LST,[B],CEC).
% this handles final case: list<->cm/prim
cecext([X],XP,CEC) :- not(is_list(XP)), !, cecextt(X,XP,CEC).
cecext(X,[XP],CEC) :- not(is_list(X)),  !, cecextt(X,XP,CEC).
% now we just have list vs list left
cecext([],[],[]) :- !.
% neither are sums: normal pairwise step
cecext([X1|LST1],[X2|LST2],CEC) :- X1\=pri((sum,_),_), X2\=pri((sum,_),_), !, cecextt(X1,X2,CEC1), cecextt(LST1,LST2,CEC2), append(CEC1,CEC2,CEC).  % normal pairwise step
% both are sums
cecext([pri((sum,F),[X])|LST1],[pri((sum,_),[X])|LST2],CEC) :- cecextt([pri((sum,F),[X])|LST1],LST2,CEC).         % match left sum with right sum, drop right sum
cecext([pri((sum,_),[X])|LST1],[pri((sum,F),[X])|LST2],CEC) :- cecextt(LST1,[pri((sum,F),[X])|LST2],CEC).         % match left sum with right sum, drop left sum
cecext([M1|LST1],[M2|LST2],[mp(M1,M2)|CEC]) :- M1=pri((sum,_),[_]), M2=pri((sum,_),[_]), !, cecextt(LST1,LST2,CEC). % match left sum with right sum, drop both
% not both are sums
cecext([X1|LST1],LST2,[mp(X1,[])|CEC]) :- X1=pri((sum,_),[_]), cecextt(LST1,LST2,CEC).                                 % ignore left sum
cecext(LST1,[X2|LST2],[mp([],X2)|CEC]) :- X2=pri((sum,_),[_]), cecextt(LST1,LST2,CEC).                                 % ignore right sum
cecext([X1|LST1],[X2|LST2],[mp(X1,X2)|CEC]) :- X1=pri((sum,_),[X1P]), cecextt(X1P,X2,CEC1), cecextt(LST1,LST2,CEC2), append(CEC1,CEC2,CEC).         % match left sum with right element, drop sum
cecext([X1|LST1],[X2|LST2],[mp(X1,X2)|CEC]) :- X1=pri((sum,_),[X1P]), cecextt(X1P,X2,CEC1), cecextt([X1|LST1],LST2,CEC2), append(CEC1,CEC2,CEC).    % match left sum with right element, keep sum
cecext([X1|LST1],[X2|LST2],[mp(X1,X2)|CEC]) :- X2=pri((sum,_),[X2P]), cecextt(X1,X2P,CEC1), cecextt(LST1,LST2,CEC2), append(CEC1,CEC2,CEC).         % match left element with right sum, drop sum
cecext([X1|LST1],[X2|LST2],[mp(X1,X2)|CEC]) :- X2=pri((sum,_),[X2P]), cecextt(X1,X2P,CEC1), cecextt(LST1,[X2|LST2],CEC2), append(CEC1,CEC2,CEC).    % match left element with right sum, keep sum

% tabling
cecextt(X,Y,L) :- cecext(X,Y,L), !.
cecextt(X,Y,L) :- findall(I,(cecext(X,Y,IP),list_to_set(IP,I)),LST), list_to_set(LST,SET), member(L,SET).
pwcecextt(X,Y,L) :- pwcecext(X,Y,L), !.
pwcecextt(X,Y,L) :- findall(I,(pwcecext(X,Y,IP),list_to_set(IP,I)),LST), list_to_set(LST,SET), member(L,SET).


exttoint([],[]).
exttoint([mp(A,A)|LST1],LST2) :- !, exttoint(LST1,LST2).
exttoint([mp(A,B)|LST1],[mp(A,B)|LST2]) :- exttoint(LST1,LST2).

cecint(A,B,CECI) :- cecextt(A,B,CECE), exttoint(CECE,CECI).

:- dynamic cecintstable/3.
cecints(X,Y,SET) :- cecintstable(X,Y,SET), !.
cecints(X,Y,SET) :- findall(I,(cecint(X,Y,IP),list_to_set(IP,I)),LST), list_to_set(LST,SET), assert(cecintstable(X,Y,SET)).

% cecact(M1::msg,M2::msg,C::[(profile,profile)]) ---
%    messages M1 and M2 in corresponding different profiles can be content
%    equivalent only if actor instantiation constraints C are satisfied
cecact(M1,M2,C) :- cecextt(M1,M2,CEC), exttoact(CEC,C).

exttoact([mp(X,_)|_],_) :- X=cm(_,dot,bot), !, fail.
exttoact([mp(_,Y)|_],_) :- Y=cm(_,dot,bot), !, fail.
exttoact([mp(X,Y)|LST],APS) :- X=cmr(V,ACT1A,ACT1B), ACT1A\=dot, !, Y=cmr(V,ACT2A,ACT2B), zip(ACT1A,ACT2A,ACTA), zip(ACT1B,ACT2B,ACTB), exttoact(LST,ELST), append([ACTA,ACTB,ELST],APS).
exttoact([mp(_,Y)|_],_) :- Y=cmr(_,ACT1,_), ACT1\=dot, !, fail.
exttoact([mp(X,Y)|LST],APS) :- X=cm(V,ACT1,[]), ACT\=dot, Y=cm(V,ACT2,[]), !, zip(ACT1,ACT2,ACT), exttoact(LST,ELST), append(ACT,ELST,APS).
exttoact([_|LST],APS) :- exttoact(LST,APS).
exttoact([],[]).

% ceclink(P::profile,M1::msg,M2::msg,C::[(profile,profile)]) --- 
%    profile P in M1 can be linked to the corresponding profile in M2 only if
%    actor instantiation constraints C are satisfied
ceclink(P,M1,M2,RET) :- cecextt(M1,M2,CEC), exttolink(CEC,P,RET1), exttoact(CEC,RET2), append(RET1,RET2,RET).

exttolink([mp(X,Y)|_],P,[]) :- X=cmr(V,ACT1A,_), Y=cmr(V,_,_), member(P,ACT1A). % link can be established with CE constraints
exttolink([mp(X,Y)|_],P,ACT) :- X=cm(V,ACT1A,ACT1B), Y=cm(V,ACT2A,ACT2B), member(P,ACT1A), zip(ACT1A,ACT2A,ACTA), zip(ACT1B,ACT2B,ACTB), append(ACTA,ACTB,ACT).
exttolink([_|LST],P,RET) :- exttolink(LST,P,RET).


% ----- base message handling -------------------------------------------------

% contains(X,Y), X::msg, Y::ctxi: X contains context item Y
contains(X,X) :- X=cm(_,_,_).
contains(X,X) :- X=cmr(_,_,_).
contains(L,Y) :- member(I,L), contains(I,Y).
contains(pri(_,L),Y) :- member(I,L), contains(I,Y).
contains(pri((sum,FAM),L),cm((V,FAM),A,B)) :- contains(L,cm(V,A,B)).

% local(M): M contains a locally scoped message
local(pri(_,L)) :- local(L), !.
local(L) :- member(X,L), local(X), !.
local(M) :- M=cm(_,_,bot), !.
local(M) :- M=cmr(_,_,bot), !.

% xflatten: [[[[M]]]] -> [M]: flatten all lists and pri(lst)'s
xflatten([],[]) :- !.
xflatten(LST,RET) :- is_list(LST), findall(ZP,(member(Z,LST),xflatten(Z,ZP)),RETP), append(RETP,RET), !.
xflatten(pri(lst,LST), RET) :- xflatten(LST,RET), !.
xflatten(X,[X]).

% ----- rules handling --------------------------------------------------------

%eltestneededsum(pri(lst,LST),X,[]) :- member(X,LST).
eltestneededsum(M,SM,REQ) :- elneeded(M,SM,REQ), SM\=[].
eltestneededsum(M,X,REQ) :- elneeded(M,_,REQ), member(X,REQ).  % visible failure
eltestneededsum(M,X,L) :- consneededsum(M,L), member(X,L).     % reconstruction
eltestneededsum(pri((sum,FAM),[M]),MP,[]) :- putfam(FAM,M,MP).

elneededsum(M1,M2,REQ) :- eltestneededsum(M1,M2,REQ), not(member(M2,REQ)).

consneededsum(pri((sum,_),_),_) :- !, fail.
consneededsum(M,REQ) :- consneeded(M,REQ).

dblefromreq(A,A,[]).
dblefromreq(A,B,REQ) :- eltestneededsum(A,AP,REQ1), dblefromreq(AP,B,REQ2), append(REQ1,REQ2,REQ).
dblereq(KB,M,REQ) :- member(MP,KB),dblefromreq(MP,M,REQ).


% ----- constraint handling (constraints in DNF form) -------------------------

% minimals: +LSTARG::[[msg]], -SET2::[[msg]]: given DNF constraints, eliminate
%                                             implied ones
minimals(LSTARG,SET2) :-
  findall(REQO,(member(REQ,LSTARG),list_to_ord_set(REQ,REQO)),LST1),
  findall(Z,(member(Z,LST1),not((member(Z2,LST1),ord_subset(Z2,Z),not(ord_subset(Z,Z2))))),LST2),
  list_to_ord_set(LST2,SET2).

% LST1::[[msg]], LST2::[[msg]], LST::[[msg]]: concatenations of items of LST1,LST2
minicross(LST1,LST2,LST) :- 
  ord_intersection(LST1,LST2,INT,S2M1),
  ord_subtract(LST1,LST2,S1M2),
  findall(I,(member(I1,S2M1),member(I2,S1M2),append(I1,I2,I)),DIFF),
  ord_union(INT,DIFF,INTDIFF),
  minimals(INTDIFF,LST).

% cross product of list of DNF constraints: [[[msg]]]->[[msg]] 
minicrosses([],[]).
minicrosses([X],X).
minicrosses([X|LST],RET) :- minicrosses(LST,RETP), minicross(X,RETP,RET).

